es:ES, Q, R:(EE), B:Type, f:Top. Q-R-glued(es; B; f; p-first([]); Q; p-first([]); R) 

latex

Definitions

False, {x:A| B(x)} , left + right, P  Q, Dec(P), Void, let x,y = A in B(x;y), t.1, E, t  T, b, AbsInterface(A), f(a), P  Q, x:A. B(x), X(e), s = t, , x:AB(x), x:A  B(x), P & Q, x:A. B(x), Type, e c e', <a, b>, Unit, can-apply(f;x), e  X, Q ==f== P, E(X), Inj(A;B;f), f is Q-R-pre-preserving on P, {I}, Q = f== P, g glues Ia:Qa f Ib:Rb, Q-R-glued(es; Ib_valtype; f; Ia; Qa; Ib; Rb), p-first(L), ES, Top, [], , x.A(x)

Lemmas

top wf, event system wf, es-E wf, it wf, es-causle wf, false wf, es-interface-val wf, decidable false